;;;; Created on 2012-11-26 18:44:35
(defun wfp-checkerFOL (wfp)
  "Checks to see if the argument is a correct well formed proposition."
;  (write-line (format nil "----------------------------" ))
;  (write-line  (format nil "sentence:~a" wfp))
;  (write-line (format nil "Length: ~a" (length  wfp)))
;  (write-line (format nil "Before hand-quant: ~a" wfp))
  (setf wfp (handle-quantifiers wfp))
;  (write-line (format nil "After hand-quant: ~a" wfp))
;  (write-line (format nil "============================"))
;  (write-line  (format nil "wfp:     ~a" wfp ))
;  (write-line  (format nil "op      : ~a" (op wfp)))
;  (write-line  (format nil "car     : ~a  : ~a" (get-length (car wfp)) (car wfp) ))
;  (write-line  (format nil "cdr     : ~a  : ~a" (get-length (cdr wfp)) (cdr wfp) ))
;  (write-line  (format nil "arg1    : ~a  : ~a" (get-length (arg1 wfp)) (arg1 wfp) ))
;  (write-line  (format nil "arg2    : ~a  : ~a" (get-length (arg2 wfp)) (arg2 wfp) ))
;  (write-line  (format nil "second  : ~a  : ~a" (get-length (second wfp)) (second wfp) ))
  
;  (write-line (format nil "============================"))
;  (if (atom wfp)  
;    (write-line (format nil "Atom-wfp: ~a" wfp) (nil))           ; means its a proposition
    (case (car wfp)               ; else check whether its a particular type of wfp
      ;==========================================
      ((or and) ;conjunction/disjunction
;        (write-line  (format nil "Or Condition:~a -- NIL" wfp))
        (wfp-FOL-listp (cdr wfp)))    ; check if each of its arguments is a wfp
      ;==========================================
      (not  ;;negated
;        (write-line  (format nil "NOT Condition:~a -- NIL" wfp))
        (if (= (length wfp) 2)
          (wfp-checkerFOL (second wfp))
          nil))
      ;==========================================
      ((IMPLIES) ; implications
;        (write-line  (format nil "IMPLIES Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      ;((EQUIV iff) ; Equivalences
      (EQUIV  ; Equivalences
;        (write-line  (format nil "EQUIV Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      ((ALL) ; implications
;        (write-line  (format nil "ALL Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      ((EXISTS) ; implications
;        (write-line  (format nil "EXISTS Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      (otherwise
        (cond
          ;==========================================
          ;; PREDICATE
          ((eq (predicatep (stringify (op wfp))) t)
          ;((eq (predicatep (stringify (arg1 wfp))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "PREDICATE???: ~a   len: ~a" (op wfp) (get-length wfp)))
            (if (> (get-length wfp) 1)
              ;(wfp-FOL-listp (arg1 wfp))
              (wfp-checkerFOL (cdr wfp))
              t))
          ;==========================================
          ;;TERM
          ((eq (termp (stringify (op wfp))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "TERM!: ~a of ~a   len: ~a" (op wfp) (arg1 wfp) (get-length wfp)))
;            (write-line  (format nil "Result: ~a" (termp (stringify (op wfp)))))
            (if (termp (stringify (op wfp)))
              (cond 
                ( (= (get-length wfp) 1)
                  ;(write-line  (format nil "~a is a term" (car wfp))))
                  t)
                ( (> (get-length wfp) 1)
                  ;(wfp-FOL-listp (cdr wfp))))
                  (wfp-checkerFOL (cdr wfp)))
                (t
                  (write-line  (format nil "Something Funny Happened")))
                  ;nil)
              )
              ;(write-line  (format nil "~a is NOT a term" (car wfp))))
              nil)
          )
          
          ;==========================================
          ;; FUNCTION
          ((eq (funcp (stringify (op wfp))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "FUNCTION! ~a of ~a" (op wfp) wfp))
            (if (> (get-length wfp) 1)
              ;(wfp-FOL-listp (cdr wfp))
              ;(wfp-checkerFOL (cdr wfp))
              (wfp-checkerFOL (cdr wfp))
              ;wfp-FOL-listp (cdr wfp))
              nil))
          ;==========================================
          ;; NESTED FUNCTION
          ((eq (funcp (stringify (car (op wfp)))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "NESTED FUNCTION! :~a of ~a" (op wfp) wfp))
            (wfp-checkerFOL (car wfp))
            
           )
          
          ;==========================================
          ;; NESTED TERM
          ((eq (termp (stringify (car (op wfp)))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "NESTED TERM :~a of ~a" (op wfp) wfp))
            (wfp-checkerFOL (car wfp))
            
           )
          ;==========================================
          ((and (eq (atom (car wfp)) t) (eq (listp wfp) t) (eq (case? (stringify (car wfp))) t))
            t
          )
        )
))))